Nuprl Lemma : decidable__implies_better 11,40

P:Q:(x:P.). Dec(P (P  Dec(Q))  Dec(P  Q
latex


ProofTree


DefinitionsP  Q, Dec(P), x:AB(x), , t  T, P  Q, A, {T}, False
Lemmasnot wf, decidable wf

origin